Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:	app(app(F,app(app(F,f),x)),x)	→ app(app(F,app(G,app(app(F,f),x))),app(f,x))

There are 4 dependency pairs:


2:	APP(app(F,app(app(F,f),x)),x)	→ APP(app(F,app(G,app(app(F,f),x))),app(f,x))
3:	APP(app(F,app(app(F,f),x)),x)	→ APP(F,app(G,app(app(F,f),x)))
4:	APP(app(F,app(app(F,f),x)),x)	→ APP(G,app(app(F,f),x))
5:	APP(app(F,app(app(F,f),x)),x)	→ APP(f,x)

The approximated dependency graph contains one SCC: {2,5}.

Tyrolean Termination Tool (0.03 seconds) --- May 3, 2006